| 1: | terms(N) | → cons(recip(sqr(N)),n__terms(n__s(N))) | |
| 2: | sqr(0) | → 0 | |
| 3: | sqr(s(X)) | → s(add(sqr(X),dbl(X))) | |
| 4: | dbl(0) | → 0 | |
| 5: | dbl(s(X)) | → s(s(dbl(X))) | |
| 6: | add(0,X) | → X | |
| 7: | add(s(X),Y) | → s(add(X,Y)) | |
| 8: | first(0,X) | → nil | |
| 9: | first(s(X),cons(Y,Z)) | → cons(Y,n__first(X,activate(Z))) | |
| 10: | half(0) | → 0 | |
| 11: | half(s(0)) | → 0 | |
| 12: | half(s(s(X))) | → s(half(X)) | |
| 13: | half(dbl(X)) | → X | |
| 14: | terms(X) | → n__terms(X) | |
| 15: | s(X) | → n__s(X) | |
| 16: | first(X1,X2) | → n__first(X1,X2) | |
| 17: | activate(n__terms(X)) | → terms(activate(X)) | |
| 18: | activate(n__s(X)) | → s(activate(X)) | |
| 19: | activate(n__first(X1,X2)) | → first(activate(X1),activate(X2)) | |
| 20: | activate(X) | → X | |
| 21: | TERMS(N) | → SQR(N) | |
| 22: | SQR(s(X)) | → S(add(sqr(X),dbl(X))) | |
| 23: | SQR(s(X)) | → ADD(sqr(X),dbl(X)) | |
| 24: | SQR(s(X)) | → SQR(X) | |
| 25: | SQR(s(X)) | → DBL(X) | |
| 26: | DBL(s(X)) | → S(s(dbl(X))) | |
| 27: | DBL(s(X)) | → S(dbl(X)) | |
| 28: | DBL(s(X)) | → DBL(X) | |
| 29: | ADD(s(X),Y) | → S(add(X,Y)) | |
| 30: | ADD(s(X),Y) | → ADD(X,Y) | |
| 31: | FIRST(s(X),cons(Y,Z)) | → ACTIVATE(Z) | |
| 32: | HALF(s(s(X))) | → S(half(X)) | |
| 33: | HALF(s(s(X))) | → HALF(X) | |
| 34: | ACTIVATE(n__terms(X)) | → TERMS(activate(X)) | |
| 35: | ACTIVATE(n__terms(X)) | → ACTIVATE(X) | |
| 36: | ACTIVATE(n__s(X)) | → S(activate(X)) | |
| 37: | ACTIVATE(n__s(X)) | → ACTIVATE(X) | |
| 38: | ACTIVATE(n__first(X1,X2)) | → FIRST(activate(X1),activate(X2)) | |
| 39: | ACTIVATE(n__first(X1,X2)) | → ACTIVATE(X1) | |
| 40: | ACTIVATE(n__first(X1,X2)) | → ACTIVATE(X2) | |